(set-logic QF_LRA)
(declare-fun _substvar_1393_ () Bool)
(declare-fun _substvar_1652_ () Bool)
(declare-fun v6 () Bool)
(declare-fun r0 () Real)
(declare-fun r1 () Real)
(declare-fun r6 () Real)
(assert (= v6 (> r0 0.0 r1 0.64 r6 0.0)))
(push 1)
(declare-fun v10 () Bool)
(push 1)
(declare-fun v11 () Bool)
(declare-fun r7 () Real)
(declare-fun v12 () Bool)
(declare-fun r8 () Real)
(push 1)
(assert v6)
(declare-fun v13 () Bool)
(check-sat)
(declare-fun v14 () Bool)
(push 1)
(declare-fun v15 () Bool)
(declare-fun r9 () Real)
(declare-fun v16 () Bool)
(declare-fun v17 () Bool)
(declare-fun r10 () Real)
(push 1)
(declare-fun v18 () Bool)
(pop 1)
(declare-fun v19 () Bool)
(declare-fun v20 () Bool)
(pop 1)
(declare-fun r11 () Real)
(declare-fun v21 () Bool)
(push 1)
(declare-fun v22 () Bool)
(declare-fun r12 () Real)
(pop 1)
(declare-fun v23 () Bool)
(declare-fun r13 () Real)
(pop 1)
(declare-fun v24 () Bool)
(declare-fun r14 () Real)
(pop 1)
(declare-fun v25 () Bool)
(declare-fun r15 () Real)
(push 1)
(declare-fun v26 () Bool)
(push 1)
(declare-fun v27 () Bool)
(push 1)
(declare-fun v28 () Bool)
(declare-fun v29 () Bool)
(declare-fun r16 () Real)
(declare-fun v30 () Bool)
(push 1)
(declare-fun v31 () Bool)
(declare-fun r17 () Real)
(pop 1)
(declare-fun v32 () Bool)
(push 1)
(declare-fun v33 () Bool)
(declare-fun r18 () Real)
(push 1)
(declare-fun v34 () Bool)
(pop 1)
(declare-fun v35 () Bool)
(declare-fun v36 () Bool)
(declare-fun v37 () Bool)
(declare-fun v38 () Bool)
(declare-fun v39 () Bool)
(declare-fun v40 () Bool)
(declare-fun v41 () Bool)
(declare-fun r19 () Real)
(pop 1)
(declare-fun v42 () Bool)
(declare-fun r20 () Real)
(pop 1)
(declare-fun v43 () Bool)
(declare-fun v44 () Bool)
(declare-fun r21 () Real)
(push 1)
(declare-fun v45 () Bool)
(declare-fun r22 () Real)
(pop 1)
(declare-fun v46 () Bool)
(push 1)
(declare-fun v47 () Bool)
(declare-fun v48 () Bool)
(declare-fun v49 () Bool)
(pop 1)
(declare-fun v50 () Bool)
(declare-fun r23 () Real)
(push 1)
(declare-fun v51 () Bool)
(declare-fun r24 () Real)
(declare-fun v52 () Bool)
(declare-fun r25 () Real)
(declare-fun v53 () Bool)
(declare-fun r26 () Real)
(pop 1)
(declare-fun r27 () Real)
(pop 1)
(push 1)
(declare-fun r28 () Real)
(declare-fun v54 () Bool)
(pop 1)
(declare-fun v55 () Bool)
(pop 1)
(declare-fun v56 () Bool)
(push 1)
(push 1)
(declare-fun v57 () Bool)
(push 1)
(declare-fun v58 () Bool)
(declare-fun v59 () Bool)
(declare-fun r29 () Real)
(check-sat)
(declare-fun r30 () Real)
(pop 1)
(declare-fun v60 () Bool)
(declare-fun r31 () Real)
(push 1)
(declare-fun v61 () Bool)
(push 1)
(declare-fun v62 () Bool)
(declare-fun v63 () Bool)
(declare-fun r32 () Real)
(declare-fun v64 () Bool)
(declare-fun v65 () Bool)
(declare-fun v66 () Bool)
(declare-fun r33 () Real)
(pop 1)
(declare-fun v67 () Bool)
(assert false)
(declare-fun v68 () Bool)
(push 1)
(declare-fun v69 () Bool)
(pop 1)
(declare-fun v70 () Bool)
(declare-fun r34 () Real)
(declare-fun v71 () Bool)
(declare-fun r35 () Real)
(declare-fun r36 () Real)
(push 1)
(declare-fun v72 () Bool)
(declare-fun r37 () Real)
(push 1)
(declare-fun v73 () Bool)
(declare-fun v74 () Bool)
(declare-fun r38 () Real)
(declare-fun v75 () Bool)
(check-sat)
(push 1)
(declare-fun v76 () Bool)
(push 1)
(declare-fun v77 () Bool)
(declare-fun r39 () Real)
(pop 1)
(declare-fun v78 () Bool)
(declare-fun r40 () Real)
(declare-fun v81 () Bool)
(push 1)
(declare-fun v82 () Bool)
(declare-fun v83 () Bool)
(pop 1)
(declare-fun v84 () Bool)
(declare-fun r41 () Real)
(pop 1)
(declare-fun v85 () Bool)
(pop 1)
(declare-fun v86 () Bool)
(declare-fun v87 () Bool)
(declare-fun v88 () Bool)
(push 1)
(declare-fun v89 () Bool)
(pop 1)
(declare-fun v90 () Bool)
(push 1)
(declare-fun v91 () Bool)
(push 1)
(declare-fun v92 () Bool)
(declare-fun v93 () Bool)
(declare-fun r43 () Real)
(pop 1)
(declare-fun r44 () Real)
(push 1)
(declare-fun v94 () Bool)
(declare-fun r45 () Real)
(pop 1)
(declare-fun v95 () Bool)
(declare-fun v96 () Bool)
(declare-fun r46 () Real)
(declare-fun v97 () Bool)
(pop 1)
(declare-fun r47 () Real)
(push 1)
(declare-fun v98 () Bool)
(declare-fun v99 () Bool)
(declare-fun r48 () Real)
(declare-fun v100 () Bool)
(declare-fun r49 () Real)
(pop 1)
(declare-fun v101 () Bool)
(declare-fun r50 () Real)
(pop 1)
(declare-fun v102 () Bool)
(push 1)
(declare-fun v103 () Bool)
(declare-fun r51 () Real)
(push 1)
(declare-fun r52 () Real)
(check-sat)
(pop 1)
(declare-fun v104 () Bool)
(declare-fun v105 () Bool)
(declare-fun r53 () Real)
(check-sat)
(push 1)
(declare-fun v106 () Bool)
(pop 1)
(declare-fun v107 () Bool)
(check-sat)
(declare-fun v108 () Bool)
(check-sat)
(declare-fun v109 () Bool)
(declare-fun r54 () Real)
(pop 1)
(declare-fun v110 () Bool)
(pop 1)
(declare-fun v111 () Bool)
(declare-fun v112 () Bool)
(declare-fun v113 () Bool)
(declare-fun r55 () Real)
(pop 1)
(declare-fun v114 () Bool)
(pop 1)
(declare-fun v115 () Bool)
(declare-fun r56 () Real)
(declare-fun r57 () Real)
(declare-fun v116 () Bool)
(declare-fun r58 () Real)
(pop 1)
(push 1)
(declare-fun v118 () Bool)
(declare-fun r59 () Real)
(declare-fun r60 () Real)
(pop 1)
(push 1)
(declare-fun v120 () Bool)
(declare-fun r61 () Real)
(pop 1)
(assert false)
(check-sat)
(push 1)
(declare-fun v123 () Bool)
(declare-fun r65 () Real)
(pop 1)
(push 1)
(declare-fun v124 () Bool)
(declare-fun v125 () Bool)
(declare-fun r67 () Real)
(declare-fun v126 () Bool)
(declare-fun r68 () Real)
(declare-fun r69 () Real)
(declare-fun v127 () Bool)
(check-sat)
(declare-fun v128 () Bool)
(declare-fun v129 () Bool)
(push 1)
(declare-fun v130 () Bool)
(declare-fun r70 () Real)
(declare-fun v131 () Bool)
(declare-fun v132 () Bool)
(push 1)
(declare-fun v133 () Bool)
(declare-fun v134 () Bool)
(declare-fun v135 () Bool)
(declare-fun r71 () Real)
(declare-fun v136 () Bool)
(check-sat)
(push 1)
(declare-fun v137 () Bool)
(declare-fun r72 () Real)
(declare-fun v138 () Bool)
(pop 1)
(declare-fun v139 () Bool)
(declare-fun r73 () Real)
(declare-fun v140 () Bool)
(pop 1)
(pop 1)
(declare-fun v141 () Bool)
(pop 1)
(check-sat)
(push 1)
(declare-fun v142 () Bool)
(declare-fun v143 () Bool)
(declare-fun v144 () Bool)
(declare-fun r74 () Real)
(declare-fun v145 () Bool)
(declare-fun v146 () Bool)
(declare-fun v147 () Bool)
(pop 1)
(push 1)
(declare-fun v148 () Bool)
(declare-fun r75 () Real)
(declare-fun r76 () Real)
(push 1)
(declare-fun v150 () Bool)
(declare-fun v151 () Bool)
(declare-fun v152 () Bool)
(declare-fun v153 () Bool)
(check-sat)
(declare-fun v154 () Bool)
(declare-fun v155 () Bool)
(declare-fun r77 () Real)
(declare-fun r78 () Real)
(declare-fun r79 () Real)
(declare-fun r80 () Real)
(pop 1)
(declare-fun v156 () Bool)
(push 1)
(declare-fun v157 () Bool)
(check-sat)
(pop 1)
(declare-fun v158 () Bool)
(declare-fun r81 () Real)
(push 1)
(declare-fun v159 () Bool)
(declare-fun r82 () Real)
(pop 1)
(declare-fun v160 () Bool)
(push 1)
(declare-fun r83 () Real)
(push 1)
(declare-fun v161 () Bool)
(declare-fun r84 () Real)
(check-sat)
(pop 1)
(declare-fun v162 () Bool)
(declare-fun r85 () Real)
(pop 1)
(declare-fun v163 () Bool)
(check-sat)
(declare-fun v164 () Bool)
(push 1)
(declare-fun v165 () Bool)
(check-sat)
(pop 1)
(declare-fun v166 () Bool)
(push 1)
(declare-fun r86 () Real)
(declare-fun v167 () Bool)
(declare-fun r87 () Real)
(declare-fun v168 () Bool)
(declare-fun r88 () Real)
(declare-fun v169 () Bool)
(declare-fun v170 () Bool)
(declare-fun v171 () Bool)
(declare-fun r89 () Real)
(push 1)
(declare-fun v172 () Bool)
(declare-fun v173 () Bool)
(declare-fun v174 () Bool)
(pop 1)
(declare-fun v175 () Bool)
(declare-fun r90 () Real)
(declare-fun v176 () Bool)
(push 1)
(declare-fun v177 () Bool)
(declare-fun v178 () Bool)
(declare-fun r91 () Real)
(declare-fun v179 () Bool)
(declare-fun r92 () Real)
(declare-fun v180 () Bool)
(push 1)
(declare-fun v181 () Bool)
(declare-fun v182 () Bool)
(declare-fun v183 () Bool)
(push 1)
(declare-fun v184 () Bool)
(declare-fun r93 () Real)
(push 1)
(declare-fun v185 () Bool)
(declare-fun r94 () Real)
(declare-fun v186 () Bool)
(declare-fun v187 () Bool)
(declare-fun r95 () Real)
(push 1)
(declare-fun v188 () Bool)
(declare-fun v189 () Bool)
(pop 1)
(declare-fun v190 () Bool)
(declare-fun r96 () Real)
(declare-fun v191 () Bool)
(declare-fun r97 () Real)
(declare-fun v192 () Bool)
(declare-fun r98 () Real)
(pop 1)
(declare-fun r99 () Real)
(push 1)
(declare-fun v193 () Bool)
(declare-fun r100 () Real)
(push 1)
(declare-fun v194 () Bool)
(pop 1)
(declare-fun v195 () Bool)
(declare-fun v196 () Bool)
(push 1)
(declare-fun v197 () Bool)
(declare-fun v198 () Bool)
(declare-fun r101 () Real)
(declare-fun v199 () Bool)
(declare-fun r102 () Real)
(check-sat)
(declare-fun v200 () Bool)
(declare-fun r103 () Real)
(push 1)
(declare-fun v201 () Bool)
(declare-fun r104 () Real)
(declare-fun r105 () Real)
(declare-fun v202 () Bool)
(push 1)
(declare-fun r106 () Real)
(declare-fun v203 () Bool)
(declare-fun r107 () Real)
(declare-fun v204 () Bool)
(declare-fun v205 () Bool)
(push 1)
(declare-fun r108 () Real)
(declare-fun r109 () Real)
(pop 1)
(declare-fun v206 () Bool)
(push 1)
(declare-fun v207 () Bool)
(push 1)
(declare-fun r110 () Real)
(declare-fun v208 () Bool)
(declare-fun v209 () Bool)
(declare-fun r111 () Real)
(declare-fun v210 () Bool)
(declare-fun v211 () Bool)
(push 1)
(declare-fun v212 () Bool)
(push 1)
(declare-fun v213 () Bool)
(push 1)
(declare-fun v214 () Bool)
(declare-fun v215 () Bool)
(declare-fun r112 () Real)
(declare-fun v216 () Bool)
(declare-fun r113 () Real)
(declare-fun v217 () Bool)
(declare-fun v218 () Bool)
(declare-fun r114 () Real)
(declare-fun r115 () Real)
(declare-fun v219 () Bool)
(push 1)
(declare-fun v220 () Bool)
(push 1)
(declare-fun v221 () Bool)
(pop 1)
(declare-fun v222 () Bool)
(declare-fun r117 () Real)
(pop 1)
(declare-fun r118 () Real)
(declare-fun v223 () Bool)
(declare-fun v224 () Bool)
(declare-fun v225 () Bool)
(declare-fun v226 () Bool)
(declare-fun r119 () Real)
(declare-fun v227 () Bool)
(declare-fun r120 () Real)
(declare-fun v228 () Bool)
(declare-fun r121 () Real)
(declare-fun v229 () Bool)
(declare-fun v230 () Bool)
(declare-fun v233 () Bool)
(declare-fun v234 () Bool)
(declare-fun v235 () Bool)
(declare-fun r122 () Real)
(declare-fun v236 () Bool)
(declare-fun v237 () Bool)
(declare-fun r123 () Real)
(pop 1)
(declare-fun v238 () Bool)
(push 1)
(declare-fun v239 () Bool)
(declare-fun v240 () Bool)
(pop 1)
(declare-fun r124 () Real)
(declare-fun r125 () Real)
(declare-fun v241 () Bool)
(declare-fun r126 () Real)
(pop 1)
(declare-fun v242 () Bool)
(declare-fun v243 () Bool)
(declare-fun r127 () Real)
(declare-fun v244 () Bool)
(declare-fun r128 () Real)
(declare-fun v245 () Bool)
(declare-fun v246 () Bool)
(push 1)
(declare-fun v247 () Bool)
(declare-fun v248 () Bool)
(declare-fun r129 () Real)
(declare-fun v249 () Bool)
(declare-fun r130 () Real)
(declare-fun v250 () Bool)
(declare-fun v251 () Bool)
(declare-fun v252 () Bool)
(declare-fun r131 () Real)
(declare-fun v253 () Bool)
(declare-fun v254 () Bool)
(declare-fun v255 () Bool)
(declare-fun r132 () Real)
(declare-fun v256 () Bool)
(declare-fun r133 () Real)
(push 1)
(declare-fun v257 () Bool)
(push 1)
(declare-fun v258 () Bool)
(declare-fun v259 () Bool)
(declare-fun r134 () Real)
(pop 1)
(declare-fun v260 () Bool)
(pop 1)
(declare-fun r135 () Real)
(push 1)
(declare-fun v261 () Bool)
(declare-fun r136 () Real)
(declare-fun v262 () Bool)
(declare-fun r137 () Real)
(declare-fun v263 () Bool)
(declare-fun v264 () Bool)
(declare-fun r138 () Real)
(declare-fun r139 () Real)
(pop 1)
(declare-fun v265 () Bool)
(declare-fun r140 () Real)
(declare-fun r141 () Real)
(declare-fun r142 () Real)
(declare-fun v266 () Bool)
(declare-fun r143 () Real)
(declare-fun v267 () Bool)
(declare-fun r144 () Real)
(pop 1)
(declare-fun v268 () Bool)
(declare-fun r145 () Real)
(declare-fun r146 () Real)
(declare-fun v270 () Bool)
(declare-fun v271 () Bool)
(declare-fun r147 () Real)
(declare-fun v272 () Bool)
(pop 1)
(declare-fun v273 () Bool)
(pop 1)
(declare-fun v274 () Bool)
(declare-fun r148 () Real)
(pop 1)
(declare-fun v275 () Bool)
(declare-fun v276 () Bool)
(push 1)
(declare-fun r149 () Real)
(pop 1)
(declare-fun r150 () Real)
(declare-fun r151 () Real)
(pop 1)
(declare-fun v277 () Bool)
(declare-fun v278 () Bool)
(push 1)
(declare-fun v279 () Bool)
(declare-fun v280 () Bool)
(declare-fun v281 () Bool)
(declare-fun v282 () Bool)
(declare-fun v283 () Bool)
(declare-fun v284 () Bool)
(push 1)
(declare-fun r152 () Real)
(declare-fun v285 () Bool)
(declare-fun r153 () Real)
(declare-fun r154 () Real)
(pop 1)
(declare-fun v286 () Bool)
(declare-fun r155 () Real)
(declare-fun v287 () Bool)
(pop 1)
(declare-fun r156 () Real)
(declare-fun v288 () Bool)
(declare-fun v289 () Bool)
(check-sat)
(declare-fun r157 () Real)
(declare-fun v290 () Bool)
(pop 1)
(declare-fun v291 () Bool)
(pop 1)
(declare-fun v292 () Bool)
(pop 1)
(declare-fun v293 () Bool)
(declare-fun r158 () Real)
(check-sat)
(declare-fun v294 () Bool)
(declare-fun v295 () Bool)
(declare-fun v296 () Bool)
(declare-fun v297 () Bool)
(push 1)
(declare-fun v298 () Bool)
(declare-fun r159 () Real)
(declare-fun v299 () Bool)
(pop 1)
(declare-fun v300 () Bool)
(declare-fun r160 () Real)
(pop 1)
(push 1)
(declare-fun v301 () Bool)
(pop 1)
(declare-fun v302 () Bool)
(declare-fun v303 () Bool)
(declare-fun v304 () Bool)
(declare-fun v305 () Bool)
(declare-fun r161 () Real)
(declare-fun v306 () Bool)
(pop 1)
(declare-fun v307 () Bool)
(declare-fun r162 () Real)
(push 1)
(declare-fun v308 () Bool)
(pop 1)
(pop 1)
(declare-fun v309 () Bool)
(declare-fun v310 () Bool)
(pop 1)
(declare-fun v311 () Bool)
(declare-fun v312 () Bool)
(push 1)
(push 1)
(declare-fun v313 () Bool)
(pop 1)
(declare-fun v314 () Bool)
(check-sat)
(declare-fun v315 () Bool)
(declare-fun v316 () Bool)
(declare-fun v317 () Bool)
(declare-fun r163 () Real)
(pop 1)
(declare-fun v318 () Bool)
(push 1)
(declare-fun v319 () Bool)
(declare-fun v320 () Bool)
(declare-fun r164 () Real)
(declare-fun r165 () Real)
(declare-fun v321 () Bool)
(declare-fun r166 () Real)
(declare-fun v322 () Bool)
(push 1)
(declare-fun v323 () Bool)
(declare-fun v324 () Bool)
(declare-fun v325 () Bool)
(declare-fun r167 () Real)
(declare-fun v326 () Bool)
(declare-fun r168 () Real)
(declare-fun r169 () Real)
(declare-fun v327 () Bool)
(declare-fun v328 () Bool)
(declare-fun r170 () Real)
(declare-fun v329 () Bool)
(push 1)
(declare-fun v330 () Bool)
(pop 1)
(declare-fun r171 () Real)
(declare-fun v331 () Bool)
(declare-fun r172 () Real)
(push 1)
(declare-fun v332 () Bool)
(declare-fun v333 () Bool)
(declare-fun r173 () Real)
(declare-fun r174 () Real)
(declare-fun v334 () Bool)
(declare-fun v335 () Bool)
(declare-fun r175 () Real)
(declare-fun v336 () Bool)
(declare-fun v337 () Bool)
(pop 1)
(declare-fun v338 () Bool)
(declare-fun v339 () Bool)
(declare-fun v340 () Bool)
(declare-fun r176 () Real)
(declare-fun v341 () Bool)
(declare-fun r177 () Real)
(declare-fun r178 () Real)
(declare-fun v342 () Bool)
(declare-fun v343 () Bool)
(declare-fun r179 () Real)
(declare-fun v344 () Bool)
(declare-fun r180 () Real)
(declare-fun v345 () Bool)
(declare-fun v346 () Bool)
(declare-fun r181 () Real)
(declare-fun r182 () Real)
(declare-fun v347 () Bool)
(declare-fun r183 () Real)
(push 1)
(declare-fun v348 () Bool)
(declare-fun v349 () Bool)
(declare-fun v350 () Bool)
(declare-fun r184 () Real)
(pop 1)
(declare-fun v351 () Bool)
(declare-fun r185 () Real)
(push 1)
(declare-fun v352 () Bool)
(declare-fun r186 () Real)
(push 1)
(declare-fun v353 () Bool)
(declare-fun r187 () Real)
(declare-fun v354 () Bool)
(declare-fun v355 () Bool)
(declare-fun v356 () Bool)
(declare-fun v357 () Bool)
(push 1)
(declare-fun v358 () Bool)
(push 1)
(push 1)
(declare-fun v359 () Bool)
(declare-fun v360 () Bool)
(declare-fun v361 () Bool)
(declare-fun r188 () Real)
(pop 1)
(declare-fun r189 () Real)
(declare-fun v362 () Bool)
(push 1)
(declare-fun v363 () Bool)
(declare-fun r190 () Real)
(push 1)
(declare-fun v364 () Bool)
(pop 1)
(declare-fun v365 () Bool)
(push 1)
(declare-fun r191 () Real)
(declare-fun v366 () Bool)
(declare-fun v367 () Bool)
(declare-fun v368 () Bool)
(declare-fun r192 () Real)
(declare-fun v369 () Bool)
(declare-fun r193 () Real)
(declare-fun v370 () Bool)
(pop 1)
(declare-fun v371 () Bool)
(declare-fun v372 () Bool)
(declare-fun r194 () Real)
(declare-fun v373 () Bool)
(pop 1)
(declare-fun r195 () Real)
(declare-fun r196 () Real)
(declare-fun v374 () Bool)
(push 1)
(declare-fun v375 () Bool)
(push 1)
(declare-fun v376 () Bool)
(declare-fun v377 () Bool)
(declare-fun r197 () Real)
(declare-fun v378 () Bool)
(check-sat)
(push 1)
(declare-fun v379 () Bool)
(declare-fun v380 () Bool)
(pop 1)
(push 1)
(push 1)
(declare-fun r198 () Real)
(push 1)
(declare-fun v382 () Bool)
(pop 1)
(declare-fun v383 () Bool)
(declare-fun v384 () Bool)
(declare-fun r199 () Real)
(declare-fun v385 () Bool)
(declare-fun r200 () Real)
(declare-fun v386 () Bool)
(push 1)
(declare-fun v387 () Bool)
(pop 1)
(declare-fun v388 () Bool)
(declare-fun r201 () Real)
(push 1)
(declare-fun v389 () Bool)
(pop 1)
(declare-fun v390 () Bool)
(declare-fun r202 () Real)
(pop 1)
(declare-fun v391 () Bool)
(declare-fun r203 () Real)
(pop 1)
(declare-fun v392 () Bool)
(declare-fun v393 () Bool)
(push 1)
(declare-fun v394 () Bool)
(declare-fun r204 () Real)
(pop 1)
(declare-fun v395 () Bool)
(declare-fun r205 () Real)
(check-sat)
(declare-fun v396 () Bool)
(declare-fun r206 () Real)
(declare-fun v397 () Bool)
(check-sat)
(pop 1)
(declare-fun v398 () Bool)
(declare-fun v399 () Bool)
(declare-fun r207 () Real)
(pop 1)
(declare-fun v400 () Bool)
(declare-fun r208 () Real)
(declare-fun v401 () Bool)
(declare-fun v402 () Bool)
(declare-fun r209 () Real)
(push 1)
(declare-fun v403 () Bool)
(push 1)
(declare-fun v404 () Bool)
(pop 1)
(declare-fun v405 () Bool)
(declare-fun r210 () Real)
(declare-fun v406 () Bool)
(declare-fun v407 () Bool)
(declare-fun r211 () Real)
(declare-fun v408 () Bool)
(push 1)
(declare-fun v409 () Bool)
(declare-fun v410 () Bool)
(declare-fun r212 () Real)
(push 1)
(declare-fun v411 () Bool)
(declare-fun v412 () Bool)
(push 1)
(declare-fun r213 () Real)
(pop 1)
(declare-fun v413 () Bool)
(pop 1)
(declare-fun v414 () Bool)
(push 1)
(declare-fun v415 () Bool)
(declare-fun v416 () Bool)
(push 1)
(declare-fun v417 () Bool)
(push 1)
(declare-fun v418 () Bool)
(declare-fun v419 () Bool)
(declare-fun v420 () Bool)
(pop 1)
(declare-fun v421 () Bool)
(declare-fun r214 () Real)
(declare-fun r215 () Real)
(declare-fun v422 () Bool)
(declare-fun r216 () Real)
(declare-fun v423 () Bool)
(push 1)
(declare-fun v424 () Bool)
(declare-fun v425 () Bool)
(declare-fun r217 () Real)
(pop 1)
(declare-fun v426 () Bool)
(declare-fun r218 () Real)
(declare-fun v427 () Bool)
(declare-fun v428 () Bool)
(push 1)
(declare-fun v429 () Bool)
(declare-fun v430 () Bool)
(pop 1)
(declare-fun v431 () Bool)
(declare-fun v432 () Bool)
(declare-fun r219 () Real)
(declare-fun v433 () Bool)
(declare-fun v434 () Bool)
(declare-fun r220 () Real)
(declare-fun v435 () Bool)
(push 1)
(declare-fun v436 () Bool)
(declare-fun v437 () Bool)
(pop 1)
(declare-fun r221 () Real)
(pop 1)
(declare-fun v438 () Bool)
(push 1)
(declare-fun v439 () Bool)
(declare-fun v440 () Bool)
(declare-fun r222 () Real)
(pop 1)
(declare-fun v441 () Bool)
(declare-fun r223 () Real)
(declare-fun r224 () Real)
(pop 1)
(declare-fun v442 () Bool)
(push 1)
(declare-fun v443 () Bool)
(declare-fun r225 () Real)
(declare-fun v444 () Bool)
(pop 1)
(declare-fun v445 () Bool)
(check-sat)
(pop 1)
(declare-fun v446 () Bool)
(push 1)
(declare-fun v447 () Bool)
(declare-fun r226 () Real)
(declare-fun v448 () Bool)
(declare-fun v449 () Bool)
(declare-fun v450 () Bool)
(push 1)
(declare-fun v451 () Bool)
(declare-fun r227 () Real)
(declare-fun r228 () Real)
(pop 1)
(declare-fun v452 () Bool)
(pop 1)
(declare-fun r229 () Real)
(declare-fun v453 () Bool)
(declare-fun v454 () Bool)
(declare-fun v455 () Bool)
(pop 1)
(declare-fun v456 () Bool)
(declare-fun r230 () Real)
(declare-fun v457 () Bool)
(declare-fun r231 () Real)
(declare-fun r232 () Real)
(push 1)
(declare-fun v458 () Bool)
(declare-fun r233 () Real)
(push 1)
(declare-fun r234 () Real)
(pop 1)
(declare-fun r235 () Real)
(declare-fun v459 () Bool)
(declare-fun r236 () Real)
(pop 1)
(declare-fun v460 () Bool)
(declare-fun r237 () Real)
(pop 1)
(declare-fun v462 () Bool)
(pop 1)
(push 1)
(declare-fun r238 () Real)
(pop 1)
(declare-fun v463 () Bool)
(check-sat)
(push 1)
(declare-fun v464 () Bool)
(push 1)
(declare-fun v465 () Bool)
(declare-fun r239 () Real)
(declare-fun v466 () Bool)
(push 1)
(declare-fun v467 () Bool)
(declare-fun r240 () Real)
(declare-fun v468 () Bool)
(declare-fun r241 () Real)
(pop 1)
(declare-fun v469 () Bool)
(declare-fun r242 () Real)
(declare-fun v470 () Bool)
(declare-fun r243 () Real)
(declare-fun v471 () Bool)
(declare-fun v472 () Bool)
(push 1)
(declare-fun v473 () Bool)
(check-sat)
(declare-fun v474 () Bool)
(declare-fun v475 () Bool)
(declare-fun r244 () Real)
(declare-fun v476 () Bool)
(declare-fun v477 () Bool)
(check-sat)
(push 1)
(declare-fun v478 () Bool)
(declare-fun v479 () Bool)
(declare-fun r245 () Real)
(push 1)
(declare-fun v480 () Bool)
(declare-fun v481 () Bool)
(declare-fun r246 () Real)
(pop 1)
(declare-fun r247 () Real)
(declare-fun v482 () Bool)
(declare-fun r248 () Real)
(declare-fun v483 () Bool)
(pop 1)
(declare-fun v484 () Bool)
(declare-fun r249 () Real)
(push 1)
(declare-fun v485 () Bool)
(declare-fun r250 () Real)
(pop 1)
(check-sat)
(push 1)
(declare-fun r251 () Real)
(declare-fun v486 () Bool)
(declare-fun v487 () Bool)
(push 1)
(declare-fun r252 () Real)
(declare-fun v488 () Bool)
(pop 1)
(push 1)
(declare-fun v489 () Bool)
(pop 1)
(declare-fun v490 () Bool)
(pop 1)
(declare-fun v491 () Bool)
(pop 1)
(pop 1)
(declare-fun v492 () Bool)
(pop 1)
(push 1)
(declare-fun v493 () Bool)
(pop 1)
(declare-fun v494 () Bool)
(pop 1)
(declare-fun v495 () Bool)
(declare-fun r253 () Real)
(pop 1)
(pop 1)
(declare-fun v496 () Bool)
(declare-fun r254 () Real)
(push 1)
(declare-fun v497 () Bool)
(declare-fun r255 () Real)
(declare-fun r256 () Real)
(pop 1)
(push 1)
(declare-fun v498 () Bool)
(declare-fun r257 () Real)
(declare-fun v499 () Bool)
(declare-fun r258 () Real)
(declare-fun v500 () Bool)
(pop 1)
(declare-fun v501 () Bool)
(declare-fun v502 () Bool)
(declare-fun v503 () Bool)
(push 1)
(declare-fun v504 () Bool)
(declare-fun r259 () Real)
(pop 1)
(declare-fun v505 () Bool)
(pop 1)
(declare-fun v506 () Bool)
(declare-fun r260 () Real)
(declare-fun v507 () Bool)
(push 1)
(declare-fun v508 () Bool)
(declare-fun v509 () Bool)
(declare-fun v510 () Bool)
(declare-fun v511 () Bool)
(declare-fun r261 () Real)
(pop 1)
(declare-fun v512 () Bool)
(declare-fun v516 () Bool)
(declare-fun v517 () Bool)
(declare-fun v518 () Bool)
(declare-fun v520 () Bool)
(declare-fun v521 () Bool)
(declare-fun v522 () Bool)
(declare-fun v523 () Bool)
(declare-fun r264 () Real)
(pop 1)
(declare-fun v524 () Bool)
(push 1)
(declare-fun v526 () Bool)
(pop 1)
(check-sat)
(push 1)
(declare-fun v533 () Bool)
(declare-fun r270 () Real)
(push 1)
(declare-fun v534 () Bool)
(declare-fun r271 () Real)
(pop 1)
(declare-fun r272 () Real)
(declare-fun v535 () Bool)
(pop 1)
(push 1)
(declare-fun v543 () Bool)
(declare-fun v544 () Bool)
(push 1)
(declare-fun v545 () Bool)
(declare-fun r274 () Real)
(push 1)
(declare-fun v546 () Bool)
(declare-fun r275 () Real)
(declare-fun v547 () Bool)
(declare-fun v548 () Bool)
(declare-fun v549 () Bool)
(declare-fun r276 () Real)
(check-sat)
(declare-fun v550 () Bool)
(pop 1)
(declare-fun v551 () Bool)
(push 1)
(declare-fun v552 () Bool)
(push 1)
(declare-fun v553 () Bool)
(declare-fun v554 () Bool)
(declare-fun v555 () Bool)
(declare-fun r277 () Real)
(declare-fun v556 () Bool)
(pop 1)
(declare-fun v557 () Bool)
(check-sat)
(declare-fun v558 () Bool)
(check-sat)
(pop 1)
(declare-fun v559 () Bool)
(declare-fun r278 () Real)
(pop 1)
(declare-fun v560 () Bool)
(pop 1)
(push 1)
(declare-fun v563 () Bool)
(declare-fun r280 () Real)
(pop 1)
(push 1)
(declare-fun v568 () Bool)
(declare-fun r283 () Real)
(declare-fun v569 () Bool)
(declare-fun v570 () Bool)
(declare-fun v571 () Bool)
(declare-fun r284 () Real)
(declare-fun v572 () Bool)
(declare-fun r285 () Real)
(declare-fun v573 () Bool)
(push 1)
(declare-fun v574 () Bool)
(declare-fun r286 () Real)
(declare-fun v575 () Bool)
(pop 1)
(declare-fun v576 () Bool)
(push 1)
(declare-fun v577 () Bool)
(declare-fun v578 () Bool)
(declare-fun r287 () Real)
(declare-fun v579 () Bool)
(check-sat)
(pop 1)
(declare-fun v580 () Bool)
(pop 1)
(push 1)
(declare-fun v583 () Bool)
(declare-fun r289 () Real)
(declare-fun v584 () Bool)
(declare-fun r290 () Real)
(check-sat)
(declare-fun r291 () Real)
(declare-fun v585 () Bool)
(pop 1)
(push 1)
(declare-fun v586 () Bool)
(declare-fun r292 () Real)
(declare-fun v587 () Bool)
(declare-fun r293 () Real)
(pop 1)
(push 1)
(declare-fun v588 () Bool)
(declare-fun v589 () Bool)
(declare-fun v590 () Bool)
(declare-fun v591 () Bool)
(push 1)
(declare-fun r294 () Real)
(declare-fun v592 () Bool)
(check-sat)
(push 1)
(declare-fun v593 () Bool)
(declare-fun v594 () Bool)
(declare-fun r295 () Real)
(declare-fun v595 () Bool)
(pop 1)
(declare-fun v596 () Bool)
(declare-fun v597 () Bool)
(declare-fun v598 () Bool)
(declare-fun r296 () Real)
(pop 1)
(declare-fun v599 () Bool)
(declare-fun r297 () Real)
(declare-fun r298 () Real)
(pop 1)
(push 1)
(declare-fun v602 () Bool)
(declare-fun v603 () Bool)
(pop 1)
(push 1)
(declare-fun v605 () Bool)
(declare-fun v606 () Bool)
(push 1)
(declare-fun v607 () Bool)
(declare-fun v608 () Bool)
(check-sat)
(declare-fun v609 () Bool)
(declare-fun r299 () Real)
(declare-fun v610 () Bool)
(declare-fun v611 () Bool)
(declare-fun v612 () Bool)
(push 1)
(declare-fun v613 () Bool)
(declare-fun r300 () Real)
(declare-fun v614 () Bool)
(declare-fun v615 () Bool)
(declare-fun r301 () Real)
(declare-fun v616 () Bool)
(declare-fun r302 () Real)
(push 1)
(declare-fun r303 () Real)
(declare-fun v617 () Bool)
(declare-fun v618 () Bool)
(declare-fun v619 () Bool)
(push 1)
(declare-fun v620 () Bool)
(declare-fun v621 () Bool)
(push 1)
(declare-fun v622 () Bool)
(declare-fun r304 () Real)
(declare-fun v623 () Bool)
(declare-fun r305 () Real)
(pop 1)
(declare-fun r306 () Real)
(pop 1)
(declare-fun v624 () Bool)
(declare-fun v625 () Bool)
(declare-fun v626 () Bool)
(declare-fun v627 () Bool)
(declare-fun v628 () Bool)
(declare-fun v629 () Bool)
(pop 1)
(pop 1)
(declare-fun v630 () Bool)
(push 1)
(declare-fun v631 () Bool)
(declare-fun r307 () Real)
(declare-fun v632 () Bool)
(check-sat)
(declare-fun v633 () Bool)
(push 1)
(declare-fun v634 () Bool)
(declare-fun v635 () Bool)
(declare-fun r308 () Real)
(declare-fun v636 () Bool)
(declare-fun r309 () Real)
(push 1)
(declare-fun v637 () Bool)
(declare-fun r310 () Real)
(declare-fun v638 () Bool)
(push 1)
(declare-fun v639 () Bool)
(declare-fun v640 () Bool)
(declare-fun r311 () Real)
(declare-fun r312 () Real)
(declare-fun v642 () Bool)
(declare-fun r313 () Real)
(pop 1)
(declare-fun r314 () Real)
(declare-fun v643 () Bool)
(declare-fun r315 () Real)
(pop 1)
(declare-fun r316 () Real)
(pop 1)
(declare-fun v644 () Bool)
(pop 1)
(declare-fun v645 () Bool)
(declare-fun r317 () Real)
(declare-fun v646 () Bool)
(declare-fun v647 () Bool)
(declare-fun v648 () Bool)
(declare-fun v649 () Bool)
(declare-fun v650 () Bool)
(declare-fun v651 () Bool)
(pop 1)
(declare-fun v652 () Bool)
(declare-fun r318 () Real)
(declare-fun v653 () Bool)
(declare-fun r319 () Real)
(pop 1)
(push 1)
(declare-fun v655 () Bool)
(declare-fun v656 () Bool)
(pop 1)
(check-sat)
(check-sat)
(push 1)
(declare-fun v672 () Bool)
(declare-fun r329 () Real)
(declare-fun v673 () Bool)
(declare-fun v674 () Bool)
(check-sat)
(declare-fun v675 () Bool)
(declare-fun v676 () Bool)
(declare-fun r330 () Real)
(declare-fun v677 () Bool)
(declare-fun r331 () Real)
(push 1)
(declare-fun r332 () Real)
(check-sat)
(declare-fun v678 () Bool)
(declare-fun r333 () Real)
(push 1)
(declare-fun v679 () Bool)
(pop 1)
(declare-fun v680 () Bool)
(declare-fun v681 () Bool)
(pop 1)
(declare-fun v682 () Bool)
(push 1)
(declare-fun v683 () Bool)
(pop 1)
(declare-fun v684 () Bool)
(declare-fun r334 () Real)
(push 1)
(declare-fun v685 () Bool)
(pop 1)
(declare-fun v686 () Bool)
(declare-fun r335 () Real)
(pop 1)
(push 1)
(declare-fun v696 () Bool)
(declare-fun r339 () Real)
(declare-fun v697 () Bool)
(declare-fun v698 () Bool)
(declare-fun v699 () Bool)
(push 1)
(declare-fun v700 () Bool)
(push 1)
(declare-fun v701 () Bool)
(pop 1)
(declare-fun v702 () Bool)
(pop 1)
(declare-fun r340 () Real)
(push 1)
(declare-fun v703 () Bool)
(declare-fun v704 () Bool)
(declare-fun r341 () Real)
(declare-fun r342 () Real)
(declare-fun r343 () Real)
(push 1)
(declare-fun v705 () Bool)
(declare-fun v706 () Bool)
(declare-fun v707 () Bool)
(pop 1)
(declare-fun v708 () Bool)
(declare-fun v709 () Bool)
(declare-fun r344 () Real)
(declare-fun r345 () Real)
(declare-fun v710 () Bool)
(pop 1)
(declare-fun v711 () Bool)
(declare-fun r346 () Real)
(declare-fun v712 () Bool)
(check-sat)
(declare-fun v713 () Bool)
(declare-fun v714 () Bool)
(push 1)
(declare-fun v715 () Bool)
(declare-fun r347 () Real)
(declare-fun v716 () Bool)
(declare-fun v717 () Bool)
(declare-fun r348 () Real)
(declare-fun v718 () Bool)
(pop 1)
(declare-fun r349 () Real)
(pop 1)
(push 1)
(declare-fun v719 () Bool)
(declare-fun v720 () Bool)
(declare-fun v721 () Bool)
(declare-fun r350 () Real)
(declare-fun v722 () Bool)
(declare-fun r351 () Real)
(pop 1)
(push 1)
(declare-fun v730 () Bool)
(declare-fun r357 () Real)
(declare-fun v731 () Bool)
(declare-fun v732 () Bool)
(push 1)
(declare-fun v733 () Bool)
(pop 1)
(declare-fun v734 () Bool)
(declare-fun r358 () Real)
(declare-fun r359 () Real)
(pop 1)
(push 1)
(declare-fun v750 () Bool)
(pop 1)
(push 1)
(declare-fun v751 () Bool)
(declare-fun r369 () Real)
(check-sat)
(pop 1)
(push 1)
(declare-fun v755 () Bool)
(declare-fun v756 () Bool)
(declare-fun r372 () Real)
(push 1)
(declare-fun v757 () Bool)
(pop 1)
(declare-fun r373 () Real)
(declare-fun v758 () Bool)
(declare-fun v759 () Bool)
(declare-fun v760 () Bool)
(declare-fun r374 () Real)
(declare-fun v761 () Bool)
(declare-fun r375 () Real)
(declare-fun v762 () Bool)
(declare-fun v763 () Bool)
(pop 1)
(push 1)
(declare-fun v765 () Bool)
(check-sat)
(pop 1)
(check-sat)
(push 1)
(declare-fun r385 () Real)
(check-sat)
(declare-fun v777 () Bool)
(pop 1)
(assert (xor _substvar_1652_ v6 true))
(push 1)
(declare-fun v779 () Bool)
(pop 1)
(push 1)
(declare-fun v780 () Bool)
(declare-fun v781 () Bool)
(declare-fun v784 () Bool)
(declare-fun r388 () Real)
(declare-fun v785 () Bool)
(pop 1)
(push 1)
(declare-fun r396 () Real)
(declare-fun v799 () Bool)
(declare-fun v800 () Bool)
(pop 1)
(push 1)
(declare-fun v801 () Bool)
(declare-fun v802 () Bool)
(pop 1)
(push 1)
(declare-fun v804 () Bool)
(pop 1)
(push 1)
(declare-fun v806 () Bool)
(declare-fun r399 () Real)
(pop 1)
(assert (xor true true true _substvar_1393_ true v524 false))
(declare-fun v825 () Bool)
(declare-fun v826 () Bool)
(declare-fun r409 () Real)
(declare-fun v827 () Bool)
(declare-fun r410 () Real)
(declare-fun v828 () Bool)
(declare-fun r411 () Real)
(declare-fun v838 () Bool)
(declare-fun v839 () Bool)
(assert (= true true true (>= 7.0 r1 0.0 r0 3497754517.0 0.0)))

